PicNic - pi-calculus non-interference checker. (Tool paper)

摘要

PICNIC is a tool for verifying security properties of systems, namely non-interference properties of processes ex- pressed as terms of the π-calculus with two security levels and declassification primitives. More precisely, it checks whether inserting a process into two different high contexts no information leakage to the low level observers occurs. These properties are decidable over finite control processes, but decidability can be extended by compositionality also to some infinite state processes. Notably, PICNIC has been developed in Fresh O’CaML, a dialect of CaML with native support for binders and fresh/local names; thus, this work can be seen also as a non-trivial case study about the applicability of these new programming languages.